|
課程名稱 |
軟體規格與驗證
Software Specification and Verification |
|
開課學期 |
110-1 |
|
授課對象 |
管理學院 資訊管理學研究所 |
|
授課教師 |
蔡益坤 |
|
課號 |
IM7079 |
|
課程識別碼 |
725 U3220 |
|
班次 |
|
|
學分 |
3.0 |
|
全/半年 |
半年 |
|
必/選修 |
選修 |
|
上課時間 |
星期三7,8,9(14:20~17:20) |
|
上課地點 |
管二203 |
|
備註 |
總人數上限：20人
外系人數限制：8人 |
|
|
|
|
課程簡介影片 |
|
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
|
課程大綱
|
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
|
課程概述 |
This is an introductory course on formal software specification and verification, covering various formalisms, methods, and tools for specifying the properties of a software program and for verifying that the program meets its specification. We will focus on deductive (theorem proving) methods. A separate, complementary course entitled “Automatic Verification” covers algorithmic (model checking) methods. |
|
課程目標 |
The goal of this course is to acquaint the students with fundamentals of formal software verification and to prepare them for conducting research in the area.
|
|
課程要求 |
Computer Programming and Discrete Mathematics |
|
預期每週課後學習時數 |
|
|
Office Hours |
每週三 13:30~14:00
每週二 13:30~14:00 |
|
指定閱讀 |
Class Notes and Selected Readings |
|
參考書目 |
Logic for Computer Science: Foundations of Automatic Theorem Proving, J.H. Gallier, Harper & Row Publishers, 1985.
Proof Theory and Automated Deduction, J. Goubault-Larrecq and I. Mackie, Kluwer Academic Publishers, 1997.
Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004.
Foundations for Programming Languages, J.C. Mitchell, The MIT Press, 1996.
Formal Syntax and Semantics of Programming Languages, K. Slonneger and B.L. Kurtz, Addison-Wesley, 1995.
Verification of Sequential and Concurrent Programs, 2nd Edition, K.R. Apt and E.-R. Olderog, Springer-Verlag, 1997.
The Science of Programming, D. Gries, Springer-Verlag, 1981.
Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten, Springer-Verlag, 1990.
Programming from Specifications, 2nd Edition, C. Morgan, 1994.
Introduction to C program proof with Frama-C and its WP plugin, Allan Blanchard, 2020.
Software Foundations, B.C. Pierce, C. Casinghino, M. Greenberg, V. Sjöberg, and B. Yorgey.
Certified Programming with Dependent Types , A. Chilipala.
The Z Notation: A Reference Manual, 2nd Edition, J.M. Spivey, 1992.
Software Engineering with B, J.B. Wordsworth, Addison-Wesley, 1996.
Modeling in Event-B: System and Software Engineering, J.-R. Abrial, Cambridge University Press, 2010.
The Temporal Logic of Reactive and Concurrent Systems: Specification, Z. Manna and A. Pnueli, Springer-Verlag, 1992.
Temporal Verification of Reactive Systems: Safety, Z. Manna and A. Pnueli, Springer, 1995.
Temporal Verification of Reactive Systems: Progress, Z. Manna and A. Pnueli, Book Draft, 1996.
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, L. Lamport, Addison-Wesley, 2003.
Parallel Program Design: A Foundation, K.M. Chandy and J. Misra, Addison-Wesley, 1988.
A Discipline of Multiprogramming: Programming Theory for Distributed Applications, J. Misra, Springer, 2001
Beauty Is Our Business: A Birthday Salute to Edsger W. Dijkstra, Edited by W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, Springer-Verlag, 1990
The Formal Methods Page: http://formalmethods.wikia.com/wiki/Formal_methods, J. Bowen. (Note: this Web portal provides links to numerous formal methods and tools.) |
|
評量方式
(僅供參考) |
|
No. |
項目 |
百分比 |
說明 |
|
1. |
Homework Assignments |
20% |
|
2. |
Participation |
10% |
|
3. |
Final Exam |
40% |
|
4. |
Term Paper/Report |
30% |
|
|
|
週次 |
日期 |
單元主題 |
|
第1週 |
9/22 |
Introduction
Fundamentals: Propositional and First-Order Logics |
|
第2週 |
9/29 |
Fundamentals: Propositional and First-Order Logics |
|
第3週 |
10/06 |
Fundamentals: Propositional and First-Order Logics |
|
第4週 |
10/13 |
Verification Tools: Coq |
|
第5週 |
10/20 |
Verification Tools: Coq |
|
第6週 |
10/27 |
Sequential Programs: Hoare Logic |
|
第7週 |
11/03 |
Sequential Programs: Hoare Logic |
|
第8週 |
11/10 |
Predicate Transformers |
|
第9週 |
11/17 |
Procedures |
|
第10週 |
11/24 |
Verification Tools: Frama-C + Plugins |
|
第11週 |
12/01 |
Verification Tools: Frama-C + Plugins |
|
第12週 |
12/08 |
Concurrent, Reactive Systems: Owicki-Gries Method |
|
第13週 |
12/15 |
Concurrent, Reactive Systems: UNITY and Linear Temporal Logic |
|
第14週 |
12/22 |
Selected Topics: Modular/Compositional Reasoning |
|
第15週 |
12/29 |
Selected Topics: Separation Logic |
|
第16週 |
1/05 |
Final Exam |
|
第17週 |
1/12 |
Broader Picture: An Overview of Formal Methods |
|
第18週 |
1/19 |
Wrap-Up Discussions |
|